Alloy 6

Nov 4, 2021

以前のversionでも前後の状態を個々に宣言することで表現できていたが、より直観的に書けるようになった

visualizerでもその表現が見やすくなった

動的な変数を宣言

例

code:例(alloy)

pred turnOn {

Lamp.state = Off && Lamp.state' = On

}

新しい予約語

table:演算子

未来演算子 過去演算子

always P

eventually P

基準点の直後の状態で成り立つ

P until Q

その状態以降の少なくとも 1 つの状態で Q が成り立ち、かつそこまでの間ずっと P が成り立つ

P releases Q

gpt-4.icon

これらの条件は、システムの振る舞いが特定の条件下でどのように進展するかをモデル化する際に役立ちます。例えば、安全性の保証や、特定のイベントが発生するまでの一時的な条件をモデル化する際に使用できます。

具体的な使用例を考えると、例えば「システムが特定の状態に達するまで、別の安全条件が常に成立している必要がある」という状況を表現する際にreleasesを使用することができます。このような場合、Pがその特定の状態を表し、Qが安全条件を表します。

探索時のscopeとして使用する？

var

;

P ; Q

その状態で P が成り立ち、かつすぐ次の状態で Q が成り立つ

なにかのエイリアスかな？

Visualizer

https://gyazo.com/58a4c4b9ca3de7634c73e6a26b09c63e

New Config

従来のNewと同じようなもの

他の例を探索する

New Trace

同instanceで、今表示されているものとは別の時間発展の例を探索

異なる未来

New Init

別の初期状態の例を探索

New Fork

現在表示している状態から、それ以外の遷移先があるかどうかを探索

参考